package org.eclipse.iota.xtext.validation;

import java.util.ArrayList;
import java.util.List;

import org.eclipse.iota.IotaPackage;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constraint;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.Existential;
import org.eclipse.iota.model.Inclusion;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.util.IotaVariableUtil;
import org.eclipse.xtext.validation.Check;


public class IotaJavaValidator extends AbstractIotaJavaValidator {
	
	@Check
	public void validateExistential(Existential existential) {
		
		Clause clause = (Clause) existential.eContainer();
		if (clause==null) return;
		
		Property property = (Property) clause.eContainer();
		if (property==null) return;
		
		// Get a list of all variables.
		List<Variable> variables = new ArrayList<Variable>();
		variables.addAll(clause.getExistentials());
		variables.addAll(property.getParameters());
		variables.remove(existential);
		
		// Check if a variable with the same name exists already.
		for (Variable var : variables) {
			if (existential.getName().equals(var.getName())) {
				error("Duplicate variable declaration", IotaPackage.EXISTENTIAL__NAME);
			}
		}
		
		// Check if it actually used in an equation.
		boolean used = false;
		for (Constraint constraint : clause.getConstraints()) {
			
			// Constraint?
			if (constraint instanceof Equation) {
				Equation eq = (Equation) constraint;
				if (IotaVariableUtil.getUsedVariables(eq.getLeft()).contains(existential) ||
					IotaVariableUtil.getUsedVariables(eq.getRight()).contains(existential)) {
					used = true; 
					break;
				}
			}
			
			else if (constraint instanceof Inclusion) {
				if (((Inclusion) constraint).getArguments().contains(existential)) {
					used = true;
				}
			}
			
			if (used) break;
		}
		if (!used) {
			warning("Unused existential", IotaPackage.CLAUSE__EXISTENTIALS);
		}
		
	}

	@Check
	public void validateInclusion(Inclusion inclusion) {
		if (inclusion.getTarget()==null) error("Unknown predicate", IotaPackage.INCLUSION);
		else {
			Property property = inclusion.getTarget();
			if (inclusion.getArguments().size()!=property.getParameters().size()) {
				error("Invalid number of arguments", IotaPackage.INCLUSION);
			} else {
				boolean equal = true;
				for (int i=0; i<property.getParameters().size(); i++) {
					if (inclusion.getArguments().get(i)!=property.getParameters().get(i)) {
						equal = false;
						break;
					}
				}
				if (equal) warning("Trivial inclusion", IotaPackage.INCLUSION);
			}
		}
	}

	@Check
	public void validateProposition(Property property) {
		// TODO
	}

}
